function DefaultVisitedStrategy(gc)
{
  this.gc = gc;
  this.visitedContexts = [];
}

DefaultVisitedStrategy.prototype.visited =
  function(node, stack, benva, store, time)
  {
    store = this.gc(store, stack, benva);
    for ( var si = 0; si < stack.length; si++)
    {
      if (stack[si] instanceof Cont)
      {
        break;
      }
    }
    var context = this.visitedContexts.getEntry([ node, benva, time, si ]);
    if (context)
    {
      var contextStacks = context[1].stacks;
      var contextStore = context[1].store;
      for (var i = 0; i < contextStacks.length; i++)
      {
        var contextStack = contextStacks[i];
        var growth = stack.length - contextStack.length;
        if (growth >= 0)
        {
          var contextStackRoot = contextStack.slice(si);
          var stackRoot = stack.slice(si + growth);
          if (!stackSubsumes(stackRoot, contextStackRoot))
          {
            continue;
          }
//          var contextStackSi = contextStack.slice(0, si);
//          var stackSi = stack.slice(0, si);
//          if (stackSubsumes(stackSi, contextStackSi))
//          {
            var stackAdded = stack.slice(si, si + growth);
            var contextStackExisting = contextStack.slice(si, si + growth);
            if (stackSubsumes(stackAdded, contextStackExisting))
            {
              if (contextStore.subsumes(store))
              {
                return null;
              }
            }
//          }
        }
      }
//      print("JOINING at", context);
      store = store.join(contextStore);
      store = this.gc(store, stack, benva);
//      print(store.diff(contextStore));
      this.visitedContexts = this.visitedContexts.updateEntry([node, benva, time, si], {stacks:contextStacks.addFirst(stack), store:store});
      return {stack : stack, store : store};      
    }
    this.visitedContexts = this.visitedContexts.updateEntry([node, benva, time, si], {stacks:[stack], store:store});
    return {stack : stack, store : store};
  }

//DefaultVisitedStrategy.prototype.visited =
//  function(node, stack, benva, store, time)
//  {
//    store = this.gc(store, stack, benva);
//    for ( var si = 0; si < stack.length; si++)
//    {
//      if (stack[si] instanceof Cont)
//      {
//        break;
//      }
//    }
//    var stackStores = this.visitedContexts.getSetEntry([ node, benva, time, si ]);
//    for (var i = 0; i < stackStores.length; i++)
//    {
//      var stackStore = stackStores[i];
//      var contextStack = stackStore.stack;
//      var contextStore = stackStore.store;
//      var growth = stack.length - contextStack.length;
//      if (growth >= 0)
//      {
//        var contextStackRoot = contextStack.slice(si);
//        var stackRoot = stack.slice(si + growth);
//        // [1 2 3 4 3 4 5 6]
//        // [1 2 3 4 5 6]
////        if (!stackSubsumes(stackRoot, contextStackRoot))
////        {
////          continue;
////        }
//          var contextStackSi = contextStack.slice(0, si);
//          var stackSi = stack.slice(0, si);
//          if (stackSubsumes(stackSi, contextStackSi))
//          {
//            var stackAdded = stack.slice(si, si + growth);
//            var contextStackExisting = contextStack.slice(si, si + growth);
//            if (stackSubsumes(stackAdded, contextStackExisting))
//            {
//              if (contextStore.subsumes(store))
//              {
//                return null;
//              }
//  //            stack = contextStackSi.concat(contextStackExisting).concat(contextStackRoot);
//            }
//          }
//        store = store.join(contextStore);
//        store = this.gc(store, stack, benva);
//        stackStores[i] = {stack : stack, store : store};
//        this.visitedContexts = this.visitedContexts.updateEntry([ node, benva, time, si ], stackStores);
//        return {stack : stack, store : store};
//      }
//    }
//    this.visitedContexts = this.visitedContexts.updateSetEntry([ node, benva, time, si ], {stack : stack, store : store});
//    return {stack : stack, store : store};
//  }
//
//DefaultVisitedStrategy.prototype.visited =
//  function(node, stack, benva, store, time)
//  {
//    store = this.gc(store, stack, benva);
//    for ( var si = 0; si < stack.length; si++)
//    {
//      if (stack[si] instanceof Cont)
//      {
//        break;
//      }
//    }
//    var stackStores = this.visitedContexts.getSetEntry([ node, benva, time, si ]);
//    for (var i = 0; i < stackStores.length; i++)
//    {
//      var stackStore = stackStores[i];
//      var contextStack = stackStore.stack;
//      var contextStore = stackStore.store;
//      var growth = stack.length - contextStack.length;
//      if (growth >= 0)
//      {
//        var contextStackRoot = contextStack.slice(si);
//        var stackRoot = stack.slice(si + growth);
//        // [1 2 3 4 3 4 5 6]
//        // [1 2 3 4 5 6]
//        if (!stackSubsumes(contextStackRoot, stackRoot))
//        {
//          continue;
//        }
//        var contextStackSi = contextStack.slice(0, si);
//        var stackSi = stack.slice(0, si);
//        if (!stackSubsumes(contextStackSi, stackSi))
//        {
//          continue;
//        }
//        var stackAdded = stack.slice(si, si + growth);
//        var contextStackExisting = contextStack.slice(si, si + growth);
//        if (stackSubsumes(contextStackExisting, stackAdded))
//        {
//          if (contextStore.subsumes(store))
//          {
//            return null;
//          }
//          stack = contextStackSi.concat(contextStackExisting).concat(contextStackRoot);
//        }
//        store = store.join(contextStore);
//        store = this.gc(store, stack, benva);
//        stackStores[i] = {stack : stack, store : store};
//        this.visitedContexts = this.visitedContexts.updateEntry([ node, benva, time, si ], stackStores);
//        return {stack : stack, store : store};
//      }
//    }
//    this.visitedContexts = this.visitedContexts.updateSetEntry([ node, benva, time, si ], {stack : stack, store : store});
//    return {stack : stack, store : store};
//  }
//
// DefaultVisitedStrategy.prototype.visited =
// function (node, stack, benva, store, time) // TODO rename/rework (does too
// much? awkward return values)
// // maybe clients should 'return visited()' with a cont on the stack, and this
// proc can decide to return [] tasks?
// {
// store = this.gc(store, stack, benva);
//  
// var kstack = stack.filter(function (x) { return x instanceof Cont});
// var vstack = stack.filter(function (x) { return !(x instanceof Cont)});
//    
// var contextStackStoreValue = this.visitedContexts.getEntry([node, benva,
// time]);
// if (contextStackStoreValue)
// {
// // context stack: 5 4 3 2 1
// // kstack : 5 4 5 4 3 2 1
// var contextStack = contextStackStoreValue[1][0];
// var contextVstack = contextStackStoreValue[1][1];
// var contextStore = contextStackStoreValue[1][2];
//      
// // print("current kstack", kstack);
// // print("context kstack", contextStack);
// // print("current vstack", vstack);
// // print("context vstack", contextVstack);
// if (true)//stackElementsSubsume(contextVstack, vstack))
// {
// var deltaL = kstack.length - contextStack.length;
//        
// // kprefix : 5 4 (5 4 3 2 1)
// var kprefix = kstack.slice(deltaL);
// if (kprefix.equals(contextStack))
// {
// // ksuffix : (5 4) 5 4 3 2 1
// // context suffix : 5 4 (5 4) 3 2 1
// var ksuffix = kstack.slice(0, deltaL);
// var contextSuffix = kstack.slice(deltaL, deltaL * 2);
// if (ksuffix.equals(contextSuffix))
// { // "always" widening on backedge with disregard for stack eq does not seem
// to + or - impact test results
// // if (stackElementsSubsume(contextStack, kprefix) &&
// stackElementsSubsume(contextSuffix, ksuffix) && contextStore.subsumes(store))
// if (/*stackElementsSubsume(contextVstack, vstack) &&*/
// contextStore.subsumes(store))
// {
// // print("## already visited", node, stack, benva, time);
// // print(store.diff(contextStore));
// // print(store.nice(), "\n", contextStore.nice());
// // print(store.nice());
// // dreadline();
// return null; // special return value
// }
// else
// {
// // print("## not visited", node, stack, benva, time);
// // print(store.diff(contextStore));
// // dreadline();
// // print("## before widening", store.nice(), "context\n",
// contextStore.nice());
// // print("## widening with kstack", kstack, "\n-- context kstack",
// contextStack, "\n - deltaL", deltaL, "-- kprefix", kprefix, "-- ksuffix",
// ksuffix, "-- contextSuffix", contextSuffix);
// var store2 = store.join(contextStore);
// store2 = this.gc(store2, stack, benva); // original stack
// // print("## after widening and gc", store2.diff(store));
// // dreadline();
// // print("## updating", node, benva, time, "\nwith kstack", kstack, "vstack",
// vstack);
// this.visitedContexts = this.visitedContexts.updateEntry([node, benva, time],
// [kstack, vstack, store2]);
// return {stack:stack, store:store2};
// }
// }
// }
// }
// }
// else // debug
// {
// // print("## no context store value for", node, benva, time);
// // print(this.visitedContexts.entryKeys().join("\n"));
// // dreadline();
// }
//
// // print("## context", node, benva, time, "\nkstack", kstack, "vstack",
// vstack);
// this.visitedContexts = this.visitedContexts.updateEntry([node, benva, time],
// [kstack, vstack, store]);
// return {stack:stack, store:store};
// }

function stackSubsumes(stack1, stack2)
{
  var d = stack1.length - stack2.length;
  if (d < 0)
  {
    return false;
  }
  for (var i = 0; i < stack2.length; i++)
  {
    var el1 = stack1[i + d];
    var el2 = stack2[i];
    if (el1 instanceof JipdaValue)
    {
      if (!(el2 instanceof JipdaValue))
      {
        return false;
      }
      if (!(el1.subsumes(el2)))
      {
        return false;
      }      
    }
    else if (el1 instanceof Cont)
    {
      if (!(el2 instanceof Cont))
      {
        return false;
      }
      if (!(el1.equals(el2)))
      {
        return false;
      }      
    }
    else
    {
      throw new Error("cannot handle " + el1);
    }
  }
  return true;
}

